es-update-iff(es;i;x;ds;e.P(e);s.f(s))
== (x:Id. vartype(i;x)  ds(x)?Top)
== & e@i. (P(e)  (x after e) = f((state when e))) & (P(e)  (x after e) = (x when e)) 

latex

---

clarification:

es-update-iff(es;i;x;ds;e.P(e);s.f(s))
== (x:Id. es-vartype(es; i; x)  fpf-cap(ds;IdDeq;x;Top))
== & alle-at(es;i;e.(P(e)  es-after(es; x; e) = f(es-state-when(es;e))  fpf-cap(ds;IdDeq;x;Top))
== & & (P(e)  es-after(es; x; e) = es-when(es; x; e)  fpf-cap(ds;IdDeq;x;Top))) 

latex

Definitions	A & B, x:A. B(x), Id, vartype(i;x), e@i. P(e), P & Q, (state when e), P  Q, A, f(x)?z, IdDeq, Top, (x after e), x when e
FDL editor aliases	es-update-iff